(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 66))
(assert (let ((e1(_ bv85800 17)))
(let ((e2(_ bv786955 21)))
(let ((e3 (bvnor v0 v0)))
(let ((e4 (bvxnor e3 ((_ zero_extend 45) e2))))
(let ((e5 (bvmul v0 v0)))
(let ((e6 (bvmul ((_ zero_extend 49) e1) e5)))
(let ((e7 (bvugt ((_ sign_extend 45) e2) e3)))
(let ((e8 (= e1 e1)))
(let ((e9 (distinct ((_ zero_extend 45) e2) e5)))
(let ((e10 (bvsge ((_ sign_extend 49) e1) e3)))
(let ((e11 (bvult e6 e5)))
(let ((e12 (bvslt e5 e3)))
(let ((e13 (bvule e5 e6)))
(let ((e14 (bvult e6 e4)))
(let ((e15 (bvsge e6 ((_ zero_extend 45) e2))))
(let ((e16 (= e2 e2)))
(let ((e17 (bvsge ((_ sign_extend 49) e1) e6)))
(let ((e18 (bvult e3 e6)))
(let ((e19 (bvugt e1 e1)))
(let ((e20 (bvule e6 e4)))
(let ((e21 (= e5 v0)))
(let ((e22 (ite e12 e12 e16)))
(let ((e23 (and e8 e13)))
(let ((e24 (=> e17 e22)))
(let ((e25 (or e11 e10)))
(let ((e26 (=> e14 e24)))
(let ((e27 (or e9 e20)))
(let ((e28 (ite e25 e18 e15)))
(let ((e29 (ite e23 e27 e23)))
(let ((e30 (xor e21 e28)))
(let ((e31 (xor e29 e26)))
(let ((e32 (xor e31 e7)))
(let ((e33 (ite e19 e30 e32)))
e33
))))))))))))))))))))))))))))))))))

(check-sat)
